(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 81))
(declare-fun v1 () (_ BitVec 1))
(declare-fun a2 () (Array  (_ BitVec 123)  (_ BitVec 4)))
(assert (let ((e3(_ bv105526939020710412926322904 87)))
(let ((e4(_ bv23308313 25)))
(let ((e5 (bvadd e3 ((_ sign_extend 86) v1))))
(let ((e6 (bvsdiv ((_ sign_extend 6) v0) e3)))
(let ((e7 (bvadd e3 e5)))
(let ((e8 (ite (bvugt ((_ sign_extend 62) e4) e3) (_ bv1 1) (_ bv0 1))))
(let ((e9 (store a2 ((_ zero_extend 36) e5) ((_ extract 75 72) e3))))
(let ((e10 (store a2 ((_ sign_extend 36) e6) ((_ extract 42 39) v0))))
(let ((e11 (store e9 ((_ zero_extend 98) e4) ((_ extract 52 49) e3))))
(let ((e12 (select a2 ((_ zero_extend 42) v0))))
(let ((e13 (store a2 ((_ zero_extend 98) e4) ((_ zero_extend 3) e8))))
(let ((e14 (select a2 ((_ zero_extend 98) e4))))
(let ((e15 (store a2 ((_ zero_extend 119) e12) ((_ extract 61 58) e6))))
(let ((e16 (bvand ((_ sign_extend 6) v0) e3)))
(let ((e17 (bvcomp e3 ((_ sign_extend 86) v1))))
(let ((e18 (concat e14 v1)))
(let ((e19 (bvashr e6 ((_ zero_extend 6) v0))))
(let ((e20 (ite (bvsle e5 e19) (_ bv1 1) (_ bv0 1))))
(let ((e21 (bvor e12 ((_ zero_extend 3) e20))))
(let ((e22 (ite (= e7 e5) (_ bv1 1) (_ bv0 1))))
(let ((e23 (ite (bvsle ((_ zero_extend 62) e4) e5) (_ bv1 1) (_ bv0 1))))
(let ((e24 (bvshl ((_ zero_extend 80) e8) v0)))
(let ((e25 (bvugt e6 ((_ zero_extend 6) e24))))
(let ((e26 (bvult e5 ((_ sign_extend 86) e17))))
(let ((e27 (distinct v1 e17)))
(let ((e28 (bvult e6 ((_ zero_extend 82) e18))))
(let ((e29 (bvult ((_ sign_extend 86) e17) e5)))
(let ((e30 (bvsle e5 ((_ zero_extend 86) e8))))
(let ((e31 (bvugt ((_ sign_extend 3) e23) e12)))
(let ((e32 (bvule ((_ zero_extend 1) e12) e18)))
(let ((e33 (bvult ((_ zero_extend 80) e17) v0)))
(let ((e34 (= e4 ((_ sign_extend 24) e22))))
(let ((e35 (bvuge ((_ sign_extend 86) e17) e3)))
(let ((e36 (= e7 e5)))
(let ((e37 (bvsgt ((_ sign_extend 83) e21) e5)))
(let ((e38 (bvugt e19 e19)))
(let ((e39 (bvugt e7 e16)))
(let ((e40 (bvult ((_ sign_extend 62) e4) e3)))
(let ((e41 (bvuge e3 e5)))
(let ((e42 (bvsgt ((_ zero_extend 24) e8) e4)))
(let ((e43 (bvsle ((_ zero_extend 80) e23) e24)))
(let ((e44 (bvsgt e19 ((_ sign_extend 86) e17))))
(let ((e45 (= e12 e12)))
(let ((e46 (bvsle e17 e17)))
(let ((e47 (bvsle ((_ sign_extend 21) e14) e4)))
(let ((e48 (bvugt ((_ sign_extend 4) e20) e18)))
(let ((e49 (or e25 e43)))
(let ((e50 (or e46 e28)))
(let ((e51 (=> e30 e39)))
(let ((e52 (ite e42 e37 e49)))
(let ((e53 (or e31 e32)))
(let ((e54 (or e45 e53)))
(let ((e55 (xor e48 e44)))
(let ((e56 (or e36 e33)))
(let ((e57 (ite e52 e52 e38)))
(let ((e58 (and e57 e56)))
(let ((e59 (or e58 e29)))
(let ((e60 (ite e51 e47 e41)))
(let ((e61 (ite e59 e34 e34)))
(let ((e62 (xor e50 e26)))
(let ((e63 (ite e40 e60 e60)))
(let ((e64 (xor e55 e54)))
(let ((e65 (xor e62 e63)))
(let ((e66 (= e35 e27)))
(let ((e67 (= e65 e61)))
(let ((e68 (= e67 e67)))
(let ((e69 (= e66 e66)))
(let ((e70 (ite e64 e69 e68)))
(let ((e71 (and e70 (not (= e3 (_ bv0 87))))))
(let ((e72 (and e71 (not (= e3 (bvnot (_ bv0 87)))))))
e72
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
